$\forall$${\it es}$:ES, $i$, $x$, $y$:Id, ${\it Tx}$, ${\it Ty}$:Type, $P$:(${\it Tx}$$\rightarrow$${\it Ty}$$\rightarrow\mathbb{P}$), ${\it Lx}$, ${\it Ly}$:(Knd List).
\\[0ex]@$i$ only ${\it Lx}$ affect $x$:${\it Tx}$
\\[0ex]$\Rightarrow$ @$i$ only ${\it Ly}$ affect $y$:${\it Ty}$
\\[0ex]$\Rightarrow$ @$i$($x$:${\it Tx}$)
\\[0ex]$\Rightarrow$ @$i$($y$:${\it Ty}$)
\\[0ex]$\Rightarrow$ $\forall$$e$@$i$. (kind($e$) $\in$ ${\it Lx}$ @ ${\it Ly}$) $\Rightarrow$ $P$($x$ when $e$,$y$ when $e$) $\Rightarrow$ $P$(($x$ after $e$),($y$ after $e$))
\\[0ex]$\Rightarrow$ @$i$ stable ${\it state}$.$P$(${\it state}$.$x$,${\it state}$.$y$)